A:Type, l:(A List), n:. (0  n)  (n < ||l||)  (l[n]  A) 

latex

Definitions	prop{i:l}, t  T, P  Q, x:A. B(x), l[i], False, A, P  Q, int_iseg(i; j), True, T, P  Q, P  Q, A  B
Lemmas	le wf, length wf1, nth tl wf, hd wf, length nth tl, true wf, squash wf, ge wf